Message1 : A -> B : {A,NA}pkB

Message2 : B -> A : {NA,NB}pkA

Message3 : A -> B : {NB}pkB

In line 1, the agent A is the initiator of the session. Agent B is the responder. Agent A sends B her identity and a freshly generated nonce NA, both encrypted using the public key of B, pkB. Agent B receives the message, decrypts it using his secret key to obtain the identity of the initiator and the nonce NA.

In line 2, B sends back to A a message containing the nonce NA that B just received and a freshly generated nonce NB. Both are encrypted using the public key of A, pkA. The initiator A receives the message and decrypts it, A verifies that the first nonce corresponds to the nonce she sent B in line 1 and obtains nonce NB.

In line 3, A sends B the nonce NB she just received encrypted with the public key of B. B receives the message and decrypts it. Then B checks that the received nonce corresponds to NB.

This protocol is declared in SeVe language as:

#Variables
     Agents: a,b;
     Nonces: na,nb;
     Public_keys: {ka,a},{kb,b};

#Initial
      a knows {na,ka};
      b knows {nb,kb};

#Protocol_description
      a -> b : {a,na}kb;
      b -> a : {na,nb}ka;
      a -> b : {nb}kb;

#System
      Initiator: Alice;
      Responder: Bob;

#Intruder
      Intruder: Intruder;
    //Intruder_knowledge: {};

#Verification
      Data_secrecy: {na} of Alice;
      Agent_authentication: {Alice is_authenticated_with Bob using {a}};